# Exercise 1

For this exercise we have to provide loop invariants which are sufficient to prove our partial correctness triple.

Program $p_{1}$ either decreases the input by 1 if it is even, increases it by 5 if it is odd and a multiple of 6 is reached, the algorithm begins dividing as many instances of 6 before the loop conditions is reached.
The loop invariant we can choose is:

$$
\{ 2 \leq y \}\ (S2)
$$

Program $p_{2}$ calculates two sums, so we can base our invariant on the loop counter $i$.
Using the resolution approach where we solve the difference equations, we can find the loop invariant:

$$
\{ i \leq n \land x = 9 i \land y = x i + x \}\ (S2, S3)
$$

Program $p_{3}$ is similar, but either increments or decrements the loop counter depending on the initial value of $y$.
Depending on this initial value, the value 2 is continually added or subtracted, so we can choose the loop invariant:

$$
\{ z = x + 2 (y - i) \land ((y \leq 0 \land i \leq 0) \lor (y \geq 0 \land i \geq 0)) \}\ (S3)
$$

The remaining part of this exercise is found in the respective dafny file of the submission.

# Exercise 2

This exercise is found in the respective dafny file of the submission.

# Exercise 3

This exercise is found in the respective dafny file of the submission.
